home
***
CD-ROM
|
disk
|
FTP
|
other
***
search
/
Tech Arsenal 1
/
Tech Arsenal (Arsenal Computer).ISO
/
tek-04
/
prolog_2.zip
/
LOGIC.ZIP
/
WANG.PRO
< prev
Wrap
Text File
|
1987-04-03
|
3KB
|
96 lines
/* Notes from Bob:
To run this program on versions FS and higher, remove the
built-in definition of member, and "hidelog" "&", or change
"&" to another symbol.
After loading, give the goal of "start.<CR>"
The printout I got from the author indicates that the following
would be a valid test, to be entered after the prompt "Write
an argument:"
(~p & r) => ((p v q) => (r & q)).
*/
/* WANG.PRO, PDPROLOG version, BYTE, oct/86 */
/* adapted by Xavier Salazar Resines, feb/2/87 */
/* This works for all the versions: */
?-hidelog; true.
?-op(240,xfy,'<=>').
?-op(230,xfy,'=>').
?-op(220,xfy,'v').
?-op(210,xfy,'&').
?-op(200,fy,'~').
start:- print('Write an argument: \n'),read(A),nl,
print('(*) marks the main => position'),nl,
print('------------------------------'),nl,argument(A).
argument(A):- nl, test([] & [] => [] & [A]),!,nl,
print('Valid argument !'),nl,nl,print('Other: ?-start.'),nl.
argument(_):-nl,print('Invalid argument, sorry.'),nl,nl,
print('Other: ?-start.'),nl.
test(A1):- nl,print('Test ',A1),nl,rule(A1,A2,Txt),!,nl,
print(A2,' ',Txt),nl,test(A2).
test(L & [H v I|T] => R):- !,nl,print('Two branches for disjunction (*)'),nl,
print('--------------------------------'),nl,
bnch1_disj,test(L & [H|T] => R),
bnch2_disj,test(L & [I|T] => R).
test(L => R & [H & I|T]):- !,nl,print('(*) Two branches for conjunction'),nl,
print('--------------------------------'),nl,
bnch1_conj,test(L => R & [H|T]),
bnch2_conj,test(L => R & [I|T]).
test(L & [H|T] => R):- !,nl,print(' [] <- [atom] (*)'),
test([H|L] & T => R).
test(L => R & [H|T]):- !,nl,print(' (*) [] <- [atom]'),
test(L => [H|R] & T).è
test(A):- tautology(A),nl,print('Tautology.'),!,nl.
test(_):- nl,print('Can not test this step'),fail.
rule(L & [H => I|T] => R, L & [~ H v I|T] => R, 'by definition (*)').
rule(L => R & [H => I|T], L => R & [~ H v I|T], '(*) by definition').
rule(L & [H <=> I|T] => R,
L & [(H => I) & (I => H)|T] => R, 'conditionals by biconditional (*)').
rule(L => R & [H <=> I|T],
L => R & [(H => I) & (I => H)|T], '(*) conditionals by biconditional').
rule(L & [~ H|T] => R & R2,
L & T => R & [H|R2], 'from negated (*) to unnegated').
rule(L1 & L2 => R & [~ H|T],
L1 & [H|L2] => R & T, 'to unnegated (*) from negated').
rule(L & [H & I|T] => R, L & [H,I|T] => R, 'comma for conjunction (*)').
rule(L => R & [H v I|T], L => R & [H,I|T], '(*) comma for disjunction').
tautology(L & [] => R & []):- members(M,L),members(M,R).
bnch1_disj:- nl,print('Branch 1 disjunction').
bnch2_disj:- nl,print('Branch 2 disjunction').
bnch1_conj:- nl,print('Branch 1 conjunction').
bnch2_conj:- nl,print('Branch 2 conjunction').
members(H,[H|_]).
members(I,[_|T]):- members(I,T).
?- cls,nl,nl,nl,print('Write: ?-start.<RET>'),nl,
print('After do write the argument, BINARY expressions within parentheses'),
nl,nl.